Nuprl Lemma : m-sys-sub-join-left
0,22
postcript
pdf
A
,
B
:System.
A
A
B
latex
Definitions
t
T
,
x
:
A
.
B
(
x
)
,
Id
,
M1
M2
,
M(
i
)
,
D1
D2
,
A
B
,
System
Lemmas
msystem
wf
,
Id
wf
,
ma-sub-join-left
origin
A, B:System. A 
A 
B A, B:System. A A B 
Tx:A. B(x) M2 D2 B